|
| creator |
Lohmann, Niels
| | Kopp, Oliver
| | Leymann, Frank
| | Reisig, Wolfgang
| | date |
2007-09-28
| | | | description |
Choreographies offer means to capture global interactions between
business processes of different partners. BPEL4Chor has been
introduced to describe these interactions using BPEL. Currently,
there are no formal methods available to verify BPEL4Chor
choreographies. In this paper, we present how BPEL4Chor
choreographies can be verified using Petri nets. A case study
undermines that our verification techniques scale. Additionally, we
show how the verification techniques can be used to generate a stub
process for a partner taking part in a choreography. This is
especially useful when the behavior of one participant is intended
to follow the corresponding requirements of the other participants.
Thus, the missing participant behavior can be generated and the
error-prone design of that participant can be skipped.
| |